[LTL] Make ltl.delay support optional clocking - #9869

@uenoku cc

Probably we should add an operation instead of adding optional operand because we could break existing delay op's semantics.

Ok, this way seems better, i will change the RFC first and then redo this pr's commits.

@uenoku cc

@fabianschuiki cc pls 👀

I'm curious as to why this is totally necessary, won't this create semantic issues when paired with assert-property style things (so lowerings that yield clocked_assert) or other ltl.clock ops? Or are you going to add extra validation to enforce that only one clock is used across an expression like in the clocked assert validation?

I'm curious as to why this is totally necessary

The initial issue came from #8673, and its main purpose was to ensure that IR (In-Relational Analysis) had clear semantic relationships when analyzing clocks.

won't this create semantic issues when paired with assert-property style things (so lowerings that yield clocked_assert) or other ltl.clock ops?

Good question. The current VerifyClockedAssertLike pass already walks the property tree under clocked_assert and rejects any nested ltl.clock ops. This PR (PR1) only adds the ClockedDelayOp definition — at this stage, nothing produces ClockedDelayOp yet, so there's no interaction to worry about.

In the follow-up PR (PR2: InferLTLClocks), ltl.clock ops are lowered by pushing their clock info into ltl.delay → ltl.clocked_delay, and then the ltl.clock is eliminated. So after InferLTLClocks runs, the clock lives exclusively on clocked_delay ops rather than on ltl.clock.

Or are you going to add extra validation to enforce that only one clock is used across an expression like in the clocked assert validation?

That said, you're right that VerifyClockedAssertLike should be updated to also reject ClockedDelayOp with mismatched clocks under clocked_assert. I'll add that check in PR2 — the validation will verify that all ClockedDelayOp clocks in the property tree are consistent with the clocked_assert clock, similar to the existing ltl.clock rejection.

Hi @uenoku @dobios @fabianschuiki, just wanted to gently bump this. I've updated the PR based on the feedback from last week. I know everyone is busy, but could you let me know if these changes look correct or if there's anything else needed before we move forward with the next steps in this new direction? Thanks!

@uenoku @dobios @fabianschuiki, hello, it's been about a month and a half since the last update on this PR. I have follow-up PRs ready but they are currently blocked on this one, so I'd like to move this forward as soon as possible. Do you have any remaining concerns about the explicit clocked delay approach? As visible in this PR, explicit clocked delays will significantly improve CIRCT's multi-clock capabilities and enhance LTL's expressiveness. I'm ready to act on any feedback immediately, I'd love to hear your thoughts.

Hey @Clo91eaf, sorry for the delay on reviews here - I think it's a busy time for a lot of the wider infrastructure right now so I guess this slipped between the cracks.

I've just finished up making a similar change to ltl.past, so it would be great to get this through so we can clean up the dicey user-defined-semantics that the ltl.clock op introduces!

This looks like quite a big diff for the first PR in this chain, which might be part of the slow reviews (time-to-review increases superlinearly with PR length IMO) - could I suggest you trim this PR down to just the definition of the new operation, and then add things like folds and docs in smaller follow-up PRs? This should speed up the review process a lot as there's much less context to digest. If you're happy with that then ping me once the PR is updated and I'll get it reviewed as soon as I can so we can clean up all these clock semantics!